『ソフトウェア工学の道具としての形式手法 Formal Methods as Software Engineering Tools』

中島震. ソフトウェア工学の道具としての形式手法 Formal Methods as Software Engineering Tools, 2007年

ソフトウェア工学の道具としての形式手法 Formal Methods as Software Engineering Tools

1. どんなもの？

形式手法の概要の説明

2007年までの形式手法概略？が説明されている

2. 先行研究と比べてどこがすごい？

3. 技術や手法のキモはどこ？

4. どうやって有効だと検証した？

5. 議論はある？

6. 次に読むべき論文は？

IEC 61508

ISO 26262

Common Criteria

『情報システムの信頼性向上に関するガイドライン』

2006年に経済産業省が発表したもの

形式手法とは

すなわち、形式手法は、

数理論理学に基づく言語ならびに証明技法などからなる基礎理論を持つことに加えて、設計技法、ドメイン知識、などが関係する総合的な技術

である。

ref: PDFの3P

第1の使い方

形式手法の究極の目標はCorrectness by Construction(CxC)とのこと

第2の使い方 : 形式検証

Validation(検証)は記述内容が意図通りであるかを調べること

Verificationは記述内容に論理的な矛盾など、何らかの観点からの不整合があるか否かを確認すること

Formal Methods Light

「使えるとこから使い始める」

プログラム検証

第3の使い方

形式手法の中核となる言語を用いて上流成果物をデザインする

オブジェクト指向モデリング

記述内容へのReasoning

V&V(Verification&Validation)

第4の使い方

V&VのためのReasoningもツール支援でやる

開発工程時に不具合検出を目指したやり方

軽量形式手法(LFM)

仕様アニメーション

Validationに特化する方法

ツールで作ったデザインをテストデータを基に実行して確かめる

Validation through Animation

構造化設計

モデル規範型(model-oriented)

これもモデル規範型？

VICE(VDM++ In a Constraned Environment)

AspectVDM

Isabelle/HOL-ZはZ記法で書かれたものを解析するやつ

OCL、Alloy

OCLはテキストベースの言語

静的な情報構造

UML

振る舞い仕様

リアルタイム・スケジューリング